/LMAR=0/XLINE=3/FONT#0=BASL30/FONT#1=BASI30/FONT#2=BASB30/FONT#10=BAXM30/FONT#11=ZERO30/FONT#3=STA200/FONT#4=NGB25
␈↓ ↓H␈↓␈↓βS␈↓∧ Department of Computer Science, STANFORD UNIVERSITY, Stanford, California 94305

␈↓ ↓H␈↓∧Telephone 415 497-4430␈↓ 	TDecember 18, 1980 




␈↓ ↓H␈↓Professor Carlos R. Borges
␈↓ ↓H␈↓Mathematics Department
␈↓ ↓H␈↓University of California
␈↓ ↓H␈↓Davis, CA 95616

␈↓ ↓H␈↓Dear Professor Borges:

␈↓ ↓H␈↓        Martin␈α∂Davis␈α∂is␈α∂one␈α∂of␈α∂the␈α∂best␈α∂known␈α∂logicians␈α∂in␈α∂America,␈α∂and␈α∂I␈α∂am␈α∂not␈α∂quali≡ed␈α∂to
␈↓ ↓H␈↓evaluate␈αhis␈α
logical␈αwork.␈α However,␈α
I␈αknow␈αsomething␈α
of␈αhis␈αwork␈α
in␈αareas␈α
touching␈αcomputing
␈↓ ↓H␈↓and arti≡cial intelligence.

␈↓ ↓H␈↓        He␈α⊃and␈α⊃Hilary␈α⊃Putnam␈α⊂wrote␈α⊃one␈α⊃of␈α⊃the␈α⊂≡rst␈α⊃theorem␈α⊃proving␈α⊃programs␈α⊃for␈α⊂predicate
␈↓ ↓H␈↓calculus,␈αand␈αthe␈αDavis-Putnam␈αalgorithm␈αwas␈αthe␈αbenchmark␈αin␈αthis␈α≡eld␈αfor␈αa␈αnumber␈αof␈αyears.
␈↓ ↓H␈↓More␈αrecently,␈αhe␈αhas␈αbeen␈αinterested␈αin␈αprograms␈αthat␈αcheck␈αproofs␈αof␈αprogram␈αcorrectness,␈αbut␈αI
␈↓ ↓H␈↓don't␈α∪know␈α∩what␈α∪progress␈α∩he␈α∪has␈α∪made.␈α∩ A␈α∪third␈α∩recent␈α∪contribution␈α∩was␈α∪in␈α∪clarifying␈α∩the
␈↓ ↓H␈↓mathematical␈α
structure␈α
of␈α
non-monotonic␈α
reasoning.␈α
 So␈α
far␈α
he␈α
is␈α
the␈α
only␈α
mathematical␈α
logician␈α
to
␈↓ ↓H␈↓take␈αan␈αinterest␈αin␈αthese␈αproblems,␈αand␈αhis␈αrecent␈αarticle␈αin␈α␈↓↓Arti≡cial␈αIntelligence␈↓␈αwas␈αan␈αisland␈αof
␈↓ ↓H␈↓rigor and clarity in a sea of intuitive ideas.

␈↓ ↓H␈↓        On␈α∂the␈α∂basis␈α⊂of␈α∂this␈α∂work␈α∂and␈α⊂other␈α∂contacts,␈α∂I␈α∂think␈α⊂Martin␈α∂Davis␈α∂has␈α∂many␈α⊂years␈α∂of
␈↓ ↓H␈↓creative␈α
and␈α
productive␈α
work␈α
ahead␈αof␈α
him,␈α
and␈α
I␈α
look␈α
forward␈αto␈α
seeing␈α
him␈α
more␈α
often␈α
if␈αhe
␈↓ ↓H␈↓moves to the West Coast.


␈↓ ↓H␈↓Sincerely,



␈↓ ↓H␈↓John McCarthy
␈↓ ↓H␈↓Professor of Computer Science